Nuprl Definition : finite-type
11,40
postcript
pdf
finite-type(
T
) ==
n
:
.
f
:int_seg(0;
n
)
T
. surject(int_seg(0;
n
);
T
;
f
)
latex
Definitions
,
x
:
A
.
B
(
x
)
,
surject(
A
;
B
;
f
)
,
int_seg(
i
;
j
)
FDL editor aliases
finite-type
origin
n:
. f:int_seg(0; n)
T. surject(int_seg(0; n); T; f) n:. f:int_seg(0; n)T. surject(int_seg(0; n); T; f) x:A. B(x)